#pragma once
#include "PDTStatement.h"
#include "PDTExp.h"
#include "PDTBoolConst.h"

class PDTIfElse  :  public PDTStatement, public TraverseIfc <PDTIfElse , PDTNode> { public:  TRAVERSAL_IFC_IMPL(PDTIfElse )
	Z3_ast Z3guard, Z3if, Z3else, Z3endif, Z3endelse, Z3closeif;
	
public:
    enum { ConditionIdx, IfIdx, ElseIdx };

	void setCondition(PDTExpBool & condition);
	void setIfResult(PDTStatement &ifResult);
	void setElseResult(PDTStatement &elseResult);

	PDTExpBool * getCondition() const ;
	PDTStatement * getIfResult() const ;
	PDTStatement * getElseResult() const;

	PDTIfElse(PDTCodeGraph & CG);
	PDTIfElse(PDTCodeGraph & CG, PDTExpBool & condition,
                  PDTStatement & ifResult, PDTStatement & elseResult);
	NodeTypeEnum getType() { return PDTIfElse_Em;}
	bool isIfElse() { return true; }

	
	virtual bool eval(PDTCodeGraph &CG)
	{
		getCondition()->eval(CG);
		bool condition = (dynamic_cast<PDTBoolConst*>(getCondition()->nValue))->getValue();
		if (condition)
		{
			if (!(getIfResult()->eval(CG)))
				return false;
		}
		else
		{
			if (!(getElseResult()->eval(CG)))
				return false;
		}
		return true;
	}

	virtual PDTNode* clone(PDTCodeGraph& CG)
	{
		PDTNode* toReturn;
		PDTExpBool* conditionClone = (PDTExpBool*)(getCondition()->clone(CG));
		PDTStatement* ifResultClone = (PDTStatement*)(children[1]->clone(CG));
		PDTStatement* elseResultClone = (PDTStatement*)(children[2]->clone(CG));
		toReturn = new PDTIfElse(CG, *conditionClone, * ifResultClone, * elseResultClone);
		//incrementCloneID();
		//untouch();
		return toReturn;
	}

	virtual stringstream & toString(stringstream & ss) const {
		ss << "if ( ";
		PDTNode * node = getCondition();
		node->toString(ss);
		ss << " ) {" << endl;
		node = getIfResult();
		node->toString(ss);
		ss << "} else {" << endl;
		node = getElseResult();
		node->toString(ss);
		ss << "}" << endl;
		return ss;
	}
	virtual Z3_ast Z3NodeVisit (PDTZ3Visitor &ZV);
};

